FDL - Step of Proof: do-apply-p-co-restrict

Step of Proof: do-apply-p-co-restrict

11,40

Inference at *
Iof proof for Lemma do-apply-p-co-restrict:

A, B:Type, f:(A

(B + Top)), P:(A

), p:(

x:A. Dec(P(x))), x:A.

(

can-apply(p-co-restrict(f;p);x))

(do-apply(p-co-restrict(f;p);x) = do-apply(f;x))

by ((((Unfold `p-co-restrict` 0)
CollapseTHEN (((Auto

)
CollapseTHEN (((((
CoRWO "do-apply-compose" 0)
THEN (Auto

))

)
CollapseTHEN (((((RWO "can-apply-compose-iff" (-1))

CoTHEN (Auto

))

)
CollapseTHEN (((RWO "do-apply-p-co-filter" 0)
THEN (Auto

))

)

THCollapseTHEN (((All (RWO "do-apply-p-co-filter"))
CollapseTHEN (Auto

))

Co.

Definitions	p-co-restrict(f;p), f o g , x.A(x), Dec(P), s = t, P Q, P & Q, x:A B(x), P Q, b, , can-apply(f;x), do-apply(f;x), p-co-filter(f), T, x(s), f(a), x. t(x), P Q, suptype(S; T), left + right, S T, x:AB(x), Top, x:A.B(x), Void, True, t T, x:A. B(x), , Type
Lemmas	p-compose wf, p-co-filter wf, decidable wf, do-apply-compose, can-apply-compose-iff, do-apply wf, assert wf, bool wf, can-apply wf, squash wf, true wf, top wf, do-apply-p-co-filter